k:Knd, T,B:Type, l:IdLnk, ds:fpf(Id; x.Type), tg:Id, f:(decl-state(ds)TB),
es:event_system{i:l}. usends1-p(es;ds;k;T;l;tg;B;f)  prop{i:l} 

latex

Definitions

t  T, x:A. B(x), source(l), Id, loc(e), es-E(es), P  Q, alle-at(es; i; e.P(e)), es-valtype(es; e), P  Q, es-val(es; e), top, id-deq, x. t(x), fpf-cap(f; eq; x; z), es-vartype(es; i; x), decl-state(ds), es-state(es; i), es-state-when(es; e), Knd, IdLnk, fpf(A; a.B(a)), event_system{i:l}, t.1, A c B, guard(T), es-sender(es; e), es-kind(es; e), rcv(l,tg), prop{i:l}, x:A. B(x), usends1-p(es;ds;k;T;l;tg;B;f)

Lemmas

event system wf, decl-state wf, fpf wf, IdLnk wf, subtype rel wf, es-valtype wf, alle-at wf, rcv wf, Knd wf, es-kind wf, es-sender wf, es-kind-rcv, es-state-when wf, subtype rel dep function, subtype rel self, es-vartype wf, fpf-cap wf, id-deq wf, top wf, es-val wf, es-E wf, Id wf, es-loc wf, lsrc wf